Nuprl Lemma : cond-to-list_wf
11,40
postcript
pdf
A
:Type,
x
:(?
A
). ?[
x
]
(
A
List)
latex
Definitions
t
T
,
type
List
,
[]
,
[
car
/
cdr
]
,
left
+
right
,
?[
x
]
,
Type
,
Unit
,
x
:
A
.
B
(
x
)
Lemmas
unit
wf
origin
A:Type, x:(?A). ?[x] 
(A List) A:Type, x:(?A). ?[x] (A List) Tx:A. B(x)